|
In proof theory, a discipline within mathematical logic, double-negation translation, sometimes called negative translation, is a general approach for embedding classical logic into intuitionistic logic, typically by translating formulas to formulas which are classically equivalent but intuitionistically inequivalent. Particular instances of double-negation translation include Glivenko's translation for propositional logic, and the Gödel–Gentzen translation and Kuroda's translation for first-order logic. == Propositional logic == The easiest double-negation translation to describe comes from Glivenko's theorem, proved by Valery Glivenko in 1929. It maps each classical formula φ to its double negation ¬¬φ. Glivenko's theorem states: :If φ is a propositional formula, then φ is a classical tautology if and only if ¬¬φ is an intuitionistic tautology. Glivenko's theorem implies the more general statement: :If ''T'' is a set of propositional formulas, ''T *'' a set consisting of the double negated formulas of ''T'', and φ a propositional formula, then ''T'' ⊢ φ in classical logic if and only if ''T *'' ⊢ ¬¬φ in intuitionistic logic. In particular, a set of propositional formulas is intuitionistically consistent if and only if it is classically satisfiable. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Double-negation translation」の詳細全文を読む スポンサード リンク
|